FDL - Nuprl Definition : no

Nuprl Definition : no_repeats

11,40

no_repeats(T; l) ==

i,j:

. (i < ||l||)

(j < ||l||)

(

(i = j))

(

(l[i] = l[j]))

clarification:

no_repeats(T; l)
==

, j:

. (i < ||l||)

(j < ||l||)

(

(i = j

))

(

(l[i] = l[j]

T))

Definitions x:A. B(x), a < b, ||as||, P Q, , A, s = t, l[i]

FDL editor aliases no_repeats

Definitions	x:A. B(x), a < b, \|\|as\|\|, P Q, , A, s = t, l[i]
FDL editor aliases	no_repeats